PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 14:59:17 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 speed-ind.prism speed-ind.props --property change_state -const T=2100
Parsing model file "speed-ind.prism"...
Type: CTMC
Modules: S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Variables: S1 S2 S3 S4 Y Z CC XX
Parsing properties file "speed-ind.props"...
1 property:
(1) "change_state": P=? [ F<=T ((S2>80)&(S3<20)) ]
---------------------------------------------------------------------
Model checking: "change_state": P=? [ F<=T ((S2>80)&(S3<20)) ]
Property constants: T=2100
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 38 iterations in 0.05 seconds (average 0.001237, setup 0.00)
Time for model construction: 32.304 seconds.
Type: CTMC
States: 743424 (1 initial)
Transitions: 9518080
Rate matrix: 33024 nodes (187 terminal), 9518080 minterms, vars: 58r/58c
Computing probabilities...
Engine: Sparse
Number of non-absorbing states: 718848 of 743424 (96.7%)
Building sparse matrix... [n=743424, nnz=9219072, compact] [35.9 MB]
Creating vector for diagonals... [5.7 MB]
Allocating iteration vectors... [3 x 5.7 MB]
TOTAL: [58.6 MB]
Uniformisation: q.t = 2.797911 x 2100.000000 = 5875.612619
Fox-Glynn: left = 5336, right = 6527
Starting iterations...
Iteration 169 (of 6527): max relative diff=0.067337, 5.02 sec so far
Iteration 337 (of 6527): max relative diff=0.028687, 10.02 sec so far
Iteration 505 (of 6527): max relative diff=0.015675, 15.03 sec so far
Iteration 673 (of 6527): max relative diff=0.009357, 20.06 sec so far
Iteration 841 (of 6527): max relative diff=0.005872, 25.07 sec so far
Iteration 1009 (of 6527): max relative diff=0.003969, 30.07 sec so far
Iteration 1177 (of 6527): max relative diff=0.003021, 35.09 sec so far
Iteration 1345 (of 6527): max relative diff=0.002371, 40.10 sec so far
Iteration 1513 (of 6527): max relative diff=0.001908, 45.10 sec so far
Iteration 1681 (of 6527): max relative diff=0.001567, 50.11 sec so far
Iteration 1849 (of 6527): max relative diff=0.001311, 55.11 sec so far
Iteration 2017 (of 6527): max relative diff=0.001115, 60.12 sec so far
Iteration 2185 (of 6527): max relative diff=0.000962, 65.14 sec so far
Iteration 2354 (of 6527): max relative diff=0.000840, 70.17 sec so far
Iteration 2522 (of 6527): max relative diff=0.000743, 75.18 sec so far
Iteration 2690 (of 6527): max relative diff=0.000665, 80.19 sec so far
Iteration 2858 (of 6527): max relative diff=0.000600, 85.21 sec so far
Iteration 3025 (of 6527): max relative diff=0.000546, 90.23 sec so far
Iteration 3193 (of 6527): max relative diff=0.000501, 95.24 sec so far
Iteration 3361 (of 6527): max relative diff=0.000462, 100.25 sec so far
Iteration 3529 (of 6527): max relative diff=0.000428, 105.25 sec so far
Iteration 3697 (of 6527): max relative diff=0.000399, 110.27 sec so far
Iteration 3865 (of 6527): max relative diff=0.000374, 115.28 sec so far
Iteration 4033 (of 6527): max relative diff=0.000351, 120.30 sec so far
Iteration 4201 (of 6527): max relative diff=0.000331, 125.31 sec so far
Iteration 4369 (of 6527): max relative diff=0.000313, 130.31 sec so far
Iteration 4537 (of 6527): max relative diff=0.000297, 135.33 sec so far
Iteration 4705 (of 6527): max relative diff=0.000283, 140.34 sec so far
Iteration 4873 (of 6527): max relative diff=0.000269, 145.35 sec so far
Iteration 5038 (of 6527): max relative diff=0.000257, 150.36 sec so far
Iteration 5207 (of 6527): max relative diff=0.000246, 155.39 sec so far
Iteration 5374 (of 6527): max relative diff=0.000236, 160.41 sec so far
Iteration 5536 (of 6527): max relative diff=0.000227, 165.43 sec so far
Iteration 5698 (of 6527): max relative diff=0.000219, 170.46 sec so far
Iteration 5860 (of 6527): max relative diff=0.000211, 175.46 sec so far
Iteration 6018 (of 6527): max relative diff=0.000204, 180.47 sec so far
Iteration 6180 (of 6527): max relative diff=0.000197, 185.50 sec so far
Iteration 6341 (of 6527): max relative diff=0.000191, 190.51 sec so far
Iteration 6503 (of 6527): max relative diff=0.000185, 195.52 sec so far
Iterative method: 6527 iterations in 207.11 seconds (average 0.030070, setup 10.85)
Value in the initial state: 0.04229449797846471
Time for model checking: 207.129 seconds.
Result: 0.04229449797846471 (value in the initial state)
Overall running time: 240.039 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.